\documentclass[envcountsame]{llncs}

\usepackage[hmargin=1cm,vmargin=1cm]{geometry}

\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{graphicx}
\usepackage{pdflscape}
%\usepackage{algorithm2e}
\usepackage{multicol}
\usepackage{subfig}



\usepackage{bussproofs}
\usepackage{proof}
\usepackage{url}

\usepackage{fancybox}
\usepackage{fancyvrb}

% Sequent Calculus Proof Settings
\EnableBpAbbreviations
\def\fCenter{\mbox{\ $\vdash$\ }}
\newcommand{\rl}[1]{\RightLabel{#1}}

\usepackage{commands}


\title{
  {\LJe} and \iCERes%
  %\thanks{}
}

\author{
  Alexander Leitsch%\inst{1}
  \and Giselle Reis%\inst{1}
  \and %\\
  Bruno Woltzenlogel Paleo%\inst{1}
}

\authorrunning{%D.\~Deharbe \and P.\~Fontaine \and S.\~Merz \and 
B.\~Woltzenlogel Paleo}

\institute{
  Theory and Logic Group, Institut f\"{u}r Computersprachen, Technische Universit\"{a}t Wien, Vienna, Austria \\
  \email{\{leitsch, giselle, bruno\}@logic.at}
}

% ===========================================================================


\newenvironment{calculus}{\begin{center}\begin{Sbox}\begin{minipage}{0.8\textwidth}}{\end{minipage}\end{Sbox}\fbox{\TheSbox}\end{center}}


% ===========================================================================

\begin{document}

\maketitle

\begin{abstract}

\end{abstract}

\section{Introduction}


Achtung: all theorems stated in this draft are just conjectures... But I do believe they are mostly correct modulo small fixes in the definitions.
Some of the definitions are very informal, and obviously should be formalized in a final version of this paper.


\section{The Intuitionistic Sequent Calculus \LJe}
\label{section:LDe}



\begin{example}
 Skolemization does not preserve derivability in the sequent calculus {\LJ}. While $\neg \all x. P(x) \seq \ex y. \neg P(y)$ is unprovable, its skolemization is, as shown below (where $c$ is a skolem constant):
\begin{prooftree}
\AXC{$P(c) \seq P(c)$} \RightLabel{$\neg_l$}
\UIC{$\neg P(c), P(c) \seq $} \RightLabel{$\neg_r$}
\UIC{$\neg P(c) \seq \neg P(c)$} \RightLabel{$\ex_r$}
\UIC{$\neg P(c) \seq \ex y. \neg P(y)$}
\end{prooftree}
\end{example}

There are (at least) two alternative options regarding how to interpret the incompatibility between skolemization and {\LJ} exemplified above. Either one assumes that validity in intuitionistic logic is correctly captured by provability in {\LJ} (even in the presence of skolem terms), and hence skolemization is intrinsically unsound in intuitionistic logic; or one assumes that the sequent calculus {\LJ} is not prepared to deal with skolem terms appropriately. 
The former option is more traditional, but it forces skolemization to be either abandoned or modified in unusual ways (i.e. eSkolemization). Taking into account that skolemization is a rather intuitive and useful transformation, this section follows the second option and modifies the sequent calculus {\LJ} accordingly in order to forbid unsound derivations such as that shown in the example above. This is done by restricting the use of skolem terms in the instantiations performed by weak quantifer rules. However, since skolem terms are not informative enough to allow the restrictions to be specified in a local and simple way, epsilon terms are used instead.

Epsilon terms are formed with two binders: $\ep$ and $\tau$. The intended meaning of epsilon terms is given by the following epsilon axioms:
$$
\ex x. A[x] \imp A[\ep x. A[x]]
$$
$$
A[\tau x. A[x]] \imp \all x. A[x]
$$

In classical logic, the following equivalences hold, and hence one of the epsilon binders is definable using the other:
$$
A[\tau x. A[x]] \biimp \all x. A[x] \biimp \neg \ex x. \neg A[x] \biimp \neg \neg A[\ep x. \neg A[x]] \biimp A[\ep x. \neg A[x]]
$$

In intuitionistic logic, the equivalences above do not hold. Therefore, both epsilon binders are needed. Subsequently, the symbol $\nu$ is used as a meta-variable for binders: $\nu \in \{\ep, \tau \}$.

\begin{definition}
 A term $t$ is \emph{accessible} in a sequent $\Gamma \seq F$ iff it occurs in a formula $A[t]$ in the sequent and, if it contains a sub-$\nu$-term $t'$ of the the form $\nu x. B[x]$, then $A[t\{ \nu x. B[x] \mapsto x \}]$ must be a subformula of $B[x]$ .
\end{definition}


\begin{definition}
 The \emph{epsilonization} $\epsilonize{F}$ of a formula $F$ is analogous to its skolemization, but epsilon terms are used instead of skolem terms.
\end{definition}

\begin{figure}[h!]
\begin{calculus}
$$
\infer[\vee_l]{\Gamma, A \vee B \seq F}{\Gamma , A \seq F & \Gamma, B \seq F}
\quad
\infer[\vee_r^1]{\Gamma \seq A \vee B}{\Gamma \seq A}
\quad
\infer[\vee_r^2]{\Gamma \seq A \vee B}{\Gamma \seq B}
$$
\smallskip
$$
\infer[\wedge_l]{\Gamma, A \wedge B \seq F}{\Gamma, A, B \seq F}
\quad
\infer[\wedge_r]{\Gamma \seq A \wedge B}{\Gamma \seq A & \Gamma \seq B}
$$
\smallskip
$$
\infer[\imp_l]{\Gamma, A \imp B \seq F}{\Gamma \seq A & \Gamma, B \seq F}
\qquad
\infer[\imp_r]{\Gamma \seq A \imp B}{\Gamma, A \seq B}
$$
\smallskip
$$
\infer[\neg_l]{\Gamma, \neg A \seq }{\Gamma \seq A}
\qquad
\infer[\neg_r]{\Gamma \seq \neg A}{\Gamma, A \seq}
$$
\smallskip
$$
\infer[w_l]{\Gamma, A \seq F}{\Gamma \seq F}
\quad
\infer[w_r]{\Gamma \seq A}{\Gamma \seq}
\quad
\infer[c_l]{\Gamma, A \seq F}{\Gamma, A, A \seq F}
$$
\smallskip
$$
\infer[\all_l]{\Gamma, \all x. A[X]  \seq F}{\Gamma, A[t] \seq F}
\qquad
\infer[\ex_r]{\Gamma \seq \ex x. A[X]}{\Gamma \seq A[t]}
$$
\smallskip
$$
\infer[\ex_l]{\Gamma, \ex x. A[X]  \seq F}{\Gamma, A[\alpha] \seq F}
\qquad
\infer[\all_r]{\Gamma \seq \all x. A[X]}{\Gamma \seq A[\alpha]}
$$
%\smallskip
%$$
%\infer[\ex_l^{\ep}]{\Gamma, \ex x. A[X]  \seq F}{\Gamma, A[\ep x. A[x]] \seq F}
%\qquad
%\infer[\all_r^{\ep}]{\Gamma \seq \all x. A[X]}{\Gamma \seq A[\tau x. A[x]]}
%$$
\medskip
where:
\begin{itemize}
 \item $\alpha$ must satisfy the eigen-variable conditions.
 \item the term $t$ must be accessible in the conclusion sequent of a weak quantifer inference.
\end{itemize}
\end{calculus}
\caption{The intuitionistic sequent calculus \LJe}
\label{figure:LJe}
\end{figure}

\clearpage

\begin{theorem}
 A sequent $s$ is derivable in {\LJe} iff its epsilonization $\epsilonize{s}$ is derivable in {\LJe}.
\end{theorem}


\begin{example}
The epsilonization of $\neg \all x. P(x) \seq \ex y. \neg P(y)$ is $\neg P(\tau x. P(x)) \seq \ex y. \neg P(y)$. 
The epsilonized sequent is, as desired, not provable in {\LJe}: when searching for a proof in a bottom-up manner, the $\neg_l$ inference rule cannot be applied, because then the succedent of the premise would have two formulas; and the $\ex_r$ inference rule cannot be applied, because there are no accesible terms. In particular, $\tau x. P(x)$ is not accessible, because $\neg P(\tau x. P(x)) \{ \tau x. P(x) \mapsto x \}$ (i.e. $\neg P(x)$) is not a subformula of $P(x)$.
\end{example}

\begin{theorem}
If $\psi$ is an {\LJ}-proof of a sequent $s$, then $\epsilonize{\psi}$ is an {\LJe}-proof of $\epsilonize{s}$.
\end{theorem}

\begin{example}
Let $\psi$ be the {\LJ}-proof below:
\begin{prooftree}
\AXC{$P(a) \seq P(a)$} \RightLabel{$\ex_r$}
\UIC{$P(a) \seq \ex y. P(y)$}
		    \AXC{$P(\alpha) \seq P(\alpha)$} \RightLabel{$\ex_r$}
		    \UIC{$P(\alpha) \seq \ex y. P(y)$} \RightLabel{$w_l$}
		    \UIC{$Q, P(\alpha) \seq \ex y. P(y)$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\alpha) \seq \ex y. P(y)$} \RightLabel{$\ex_l$}
		    \UIC{$\ex z. (Q \wedge P(z)) \seq \ex y. P(y)$} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee \ex z. (Q \wedge P(z)) \seq \ex y. P(y)$}
			    \AXC{$P(\beta) \seq P(\beta)$} \RightLabel{$\neg_l$}
			    \UIC{$P(\beta), \neg P(\beta) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\beta), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\beta) \seq \neg \all u. \neg P(u)$} \RightLabel{$\ex_r$}
			    \UIC{$\ex y. P(y) \seq \neg \all u. \neg P(u)$} \RightLabel{$cut$}
		\BIC{$P(a) \vee \ex z. (Q \wedge P(z)) \seq \neg \all u. \neg P(u)$}  
\end{prooftree}

$\epsilonize{\psi}$ is the {\LJe}-proof below:
\begin{prooftree}
\AXC{$P(a) \seq P(a)$} \RightLabel{$\ex_r$}
\UIC{$P(a) \seq \ex y. P(y)$}
		    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\ex_r$}
		    \UIC{$P(\ep z. (Q\wedge P(z))  \ex y. P(y)$} \RightLabel{$w_l$}
		    \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq \ex y. P(y)$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq \ex y. P(y)$} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \ex y. P(y)$}
			    \AXC{$P(\beta) \seq P(\beta)$} \RightLabel{$\neg_l$}
			    \UIC{$P(\beta), \neg P(\beta) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\beta), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\beta) \seq \neg \all u. \neg P(u)$} \RightLabel{$\ex_r$}
			    \UIC{$\ex y. P(y) \seq \neg \all u. \neg P(u)$} \RightLabel{$cut$}
		\BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \neg \all u. \neg P(u)$}  
\end{prooftree}
\end{example}




\section{\iCERes}

When {\CERes} is applied to a proof in {\LJe}, the resulting derivation is an {\LK}-proof but not an {\LJe}-proof. This unfortunate effect is shown in the example below.   

\begin{example}
Consider the proof $\varphi$ below:
\begin{prooftree}
\AXC{$P(a) \seq P(a)$} \RightLabel{$\ex_r$}
\UIC{$P(a) \seq \ex y. P(y)$}
		    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\ex_r$}
		    \UIC{$P(\ep z. (Q\wedge P(z))  \ex y. P(y)$} \RightLabel{$w_l$}
		    \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq \ex y. P(y)$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq \ex y. P(y)$} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \ex y. P(y)$}
			    \AXC{$P(\beta) \seq P(\beta)$} \RightLabel{$\neg_l$}
			    \UIC{$P(\beta), \neg P(\beta) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\beta), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\beta) \seq \neg \all u. \neg P(u)$} \RightLabel{$\ex_r$}
			    \UIC{$\ex y. P(y) \seq \neg \all u. \neg P(u)$} \RightLabel{$cut$}
		\BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \neg \all u. \neg P(u)$}  
\end{prooftree}

Its clause set $\clauseset{\varphi}$ is:
$$
\{
\seq P(a), P(\ep z. (Q\wedge P(z)) \ \ ; \ \
P(\beta) \seq
\}
$$

It can be refuted by the following resolution refutation $\delta$:
\begin{prooftree}
\AXC{$\seq P(a), P(\ep z. (Q\wedge P(z))$}
    \AXC{$P(\beta) \seq$}
  \BIC{$\seq P(a)$}
	\AXC{$P(\beta) \seq$}
      \BIC{$\seq$}
\end{prooftree}

The projections are:

\begin{prooftree}
\AXC{$P(a) \seq P(a)$} 
		    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$}  \RightLabel{$w_l$}
		    \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq P(a), P(\ep z. (Q\wedge P(z))$}
\end{prooftree}

\begin{prooftree}
			    \AXC{$P(\beta) \seq P(\beta)$} \RightLabel{$\neg_l$}
			    \UIC{$P(\beta), \neg P(\beta) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\beta), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\beta) \seq \neg \all u. \neg P(u)$}
\end{prooftree}

The ACNF is:

\begin{tiny}
\begin{prooftree}
\AXC{$P(a) \seq P(a)$} 
		    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$}  \RightLabel{$w_l$}
		    \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq P(a), P(\ep z. (Q\wedge P(z))$}
			    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\neg_l$}
			    \UIC{$P(\ep z. (Q\wedge P(z)), \neg P(\ep z. (Q\wedge P(z)) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\ep z. (Q\wedge P(z)), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\ep z. (Q\wedge P(z)) \seq \neg \all u. \neg P(u)$} \RightLabel{$cut$}
		\BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq P(a), \neg \all u. \neg P(u)$}
				    \AXC{$P(a) \seq P(a)$} \RightLabel{$\neg_l$}
				    \UIC{$P(a), \neg P(a) \seq $} \RightLabel{$\all_l$}
				    \UIC{$P(a), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
				    \UIC{$P(a) \seq \neg \all u. \neg P(u)$} \RightLabel{$cut$}
      \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \neg \all u. \neg P(u)$}
\end{prooftree}
\end{tiny}
\end{example}

{\CERes} produces non-intuitionistic ACNFs because the clauses in the clause set can contain more than one literal in the succedent and because the projections can contain more than one literal in the succedents of their sequents. The most straightforward way of adapting {\CERes} so that its ACNFs are intuitionistic {\LJe}-proofs is to add disjunctions in the succedents of the clauses in the clause set and to add right disjunction rules to the projections when necessary. Since clauses may now contain disjunctive formulas, the resolution calculus must be adapted too. We must add disjunction rules to the resolution calculus, and we must allow resolution on non-atomic formulas too.

\begin{definition}[Merging of sequents]
Let $S = \Gamma \vdash A$ and $S' = \Gamma' \vdash B$ be two intuitionistic
sequents. We define the \emph{merging} operation ($\circ_i$) for these sequents as:
\begin{align*}
S \circ_i S' &= \Gamma, \Gamma' \vdash A \vee B &\text{if $A \neq B$}\\
S \circ_i S' &= \Gamma, \Gamma' \vdash A &\text{if $A = B$}
\end{align*}
\end{definition}

\begin{definition}[Intuitionistic Clause Terms]
\emph{Intuitionistic clause terms} (ICT) are $\{ \oplus, \otimes_i \}$-terms over
clause sets, i.e.:
\begin{itemize}
  \item Sets of intuitionistic clauses are ICT.
  \item If $X$ and $Y$ are ICT, then $X \oplus Y$ is an ICT.
  \item If $X$ and $Y$ are ICT, then $X \otimes_i Y$ is an ICT.
\end{itemize}
Let $| |$ be a mapping from clause terms to sets of clauses. Then:
\begin{align*}
|\mathcal{C}| &=  \mathcal{C} \text{  for a set of clauses $\mathcal{C}$}\\
|X \oplus Y| &= |X| \cup |Y|\\
|X \otimes_i Y| &= |X| \times_i |Y|
\end{align*}
where $\mathcal{C} \times_i \mathcal{D} = \{ C \circ_i D | C \in \mathcal{C}
\wedge D \in \mathcal{D} \}$.
\end{definition}

\begin{definition}[Intuitionistic Clause Set]
 The \emph{intuitionistic characteristic clause set} is built analogously to the
 usual characteristic clause set, i.e., they are build recursively from the
 axioms to the root of the tree on the following way:

 \begin{itemize}
  \item If $\nu$ is an axiom, then $ICS(\nu)$ is the sub-sequent composed only
  of the formulas that are cut-ancestors.
  \item If $\nu$ is the result of the application of a unary rule on $\mu$, then
  $ICS(\nu) = ICS(\mu)$
  \item If $\nu$ is the result of the application of a binary rule on $\mu_1$
  and $\mu_2$, we have to distinguish two cases:
  \begin{itemize}
    \item If the rule is applied to ancestors of the cut formula, then $ICS(\nu)
    = ICS(\mu_1) \oplus ICS(\mu_2)$.
    \item If the rule is not applied to ancestors of the cut formula, then
    $ICS(\nu) = ICS(\mu_1) \otimes_i ICS(\mu_2)$.
  \end{itemize}
 \end{itemize}
 
 %but whenever a clause has two literals in the right side, they are replaced by their disjunction.
\end{definition}

\begin{theorem}[Unsatisfiability of the Intuitionistic Clause Set]
 ToDo 
\end{theorem}
\begin{proof}
 ToDo
\end{proof}



\begin{definition}[Intuitionistic Projection]
 An \emph{intuitionistic projection} is built analogously to a usual projection. However, during proof-recursive construction, whenever two branches having different succedent formulas in their end-sequents need to be combined via a non-cut-pertinent inference, we must first perform $\vee_r$ inferences in the bottom of each branch, so that their succedent formulas become equal. 
\end{definition}

\begin{definition}
 The {\Rdisj} calculus is the resolution calculus where the resolution rule can be applied to non-atomic formulas (i.e. it is a propositional cut with unification) and the disjunction rules of {\LJe} are available. 
\end{definition}


\begin{example}
Consider the proof $\varphi$ below:
\begin{prooftree}
\AXC{$P(a) \seq P(a)$} \RightLabel{$\ex_r$}
\UIC{$P(a) \seq \ex y. P(y)$}
		    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\ex_r$}
		    \UIC{$P(\ep z. (Q\wedge P(z))  \ex y. P(y)$} \RightLabel{$w_l$}
		    \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq \ex y. P(y)$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq \ex y. P(y)$} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \ex y. P(y)$}
			    \AXC{$P(\beta) \seq P(\beta)$} \RightLabel{$\neg_l$}
			    \UIC{$P(\beta), \neg P(\beta) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\beta), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\beta) \seq \neg \all u. \neg P(u)$} \RightLabel{$\ex_r$}
			    \UIC{$\ex y. P(y) \seq \neg \all u. \neg P(u)$} \RightLabel{$cut$}
		\BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \neg \all u. \neg P(u)$}  
\end{prooftree}

Its intuitionistic clause set $\clauseset{\varphi}$ is:
$$
\{
\seq P(a)\vee P(\ep z. (Q\wedge P(z)) \ \ ; \ \
P(\beta) \seq
\}
$$

It can be refuted by the following {\Rdisj}-refutation $\delta$:
\begin{prooftree}
\AXC{$\seq P(a) \vee P(\ep z. (Q\wedge P(z))$}
    \AXC{$P(\beta) \seq$}
	  \AXC{$P(\gamma) \seq$} \RightLabel{$\vee_l$}
      \BIC{$P(\beta) \vee P(\gamma) $}
      \BIC{$\seq$}
\end{prooftree}

The projections are:

\begin{prooftree}
\AXC{$P(a) \seq P(a)$} \RightLabel{$\vee^1_r$}
\UIC{$P(a) \seq P(a) \vee P(\ep z. (Q\wedge P(z))$}
		    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$}  \RightLabel{$w_l$}
		    \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\vee^2_r$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq P(a) \vee P(\ep z. (Q\wedge P(z))$} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq P(a), P(\ep z. (Q\wedge P(z))$}
\end{prooftree}

\begin{prooftree}
			    \AXC{$P(\beta) \seq P(\beta)$} \RightLabel{$\neg_l$}
			    \UIC{$P(\beta), \neg P(\beta) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\beta), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\beta) \seq \neg \all u. \neg P(u)$}
\end{prooftree}

The output proof is:

\begin{tiny}
\begin{prooftree}
\AXC{$P(a) \seq P(a)$} \RightLabel{$\vee^1_r$}
\UIC{$P(a) \seq P(a) \vee P(\ep z. (Q\wedge P(z))$}
		    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$}  \RightLabel{$w_l$}
		    \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\vee^2_r$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq P(a) \vee P(\ep z. (Q\wedge P(z))$} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq P(a) \vee P(\ep z. (Q\wedge P(z))$}
				    \AXC{$P(a) \seq P(a)$} \RightLabel{$\neg_l$}
				    \UIC{$P(a), \neg P(a) \seq $} \RightLabel{$\all_l$}
				    \UIC{$P(a), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
				    \UIC{$P(a) \seq \neg \all u. \neg P(u)$}
			    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\neg_l$}
			    \UIC{$P(\ep z. (Q\wedge P(z)), \neg P(\ep z. (Q\wedge P(z)) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\ep z. (Q\wedge P(z)), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\ep z. (Q\wedge P(z)) \seq \neg \all u. \neg P(u)$}  \RightLabel{$\vee_l$}
		                \BIC{$P(a) \vee P(\ep z. (Q\wedge P(z)) \seq \neg \all u. \neg P(u)$} \RightLabel{$cut$}
      \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \neg \all u. \neg P(u)$}
\end{prooftree}
\end{tiny}

Just for comparison, this is the cut-free proof obtained by reductive methods:

\begin{prooftree}
\AXC{$P(a) \seq P(a)$} \RightLabel{$ \neg_l $}
\UIC{$P(a), \neg P(a) \seq $} \RightLabel{$ \all_l $}
\UIC{$P(a), \all y. \neg P(y) \seq $} \RightLabel{$ \neg_r $}
\UIC{$P(a) \seq \neg \all y. \neg P(y)$}
		    \AXC{$P(\alpha) \seq P(\alpha)$} \RightLabel{$ \neg_l $}
		    \UIC{$P(\alpha), \neg P(\alpha) \seq $} \RightLabel{$ \all_l $}
		    \UIC{$P(\alpha), \all y. \neg P(y) \seq $} \RightLabel{$ \neg_r $}
		    \UIC{$P(\alpha) \seq \neg \all y. \neg P(y)$} \RightLabel{$ w_l $}
		    \UIC{$Q, P(\alpha) \seq \neg \all y. \neg P(y)$} \RightLabel{$ \wedge_l $}
		    \UIC{$Q \wedge P(\alpha) \seq \neg \all y. \neg P(y)$} \RightLabel{$ \ex_l $}
		    \UIC{$\ex z. (Q \wedge P(z)) \seq \neg \all y. \neg P(y)$} \RightLabel{$ \vee_l $}
	  \BIC{$P(a) \vee \ex z. (Q \wedge P(z)) \seq \neg \all y. \neg P(y)$}
\end{prooftree}
\end{example}


\section{Intuitionistic Herbrand Sequents}

Let $\psi$ be the proof below:
\begin{prooftree}
\AXC{$P(a) \seq P(a) $} \RightLabel{$\ex_r$}
\UIC{$P(a) \seq \ex x. P(x) $}
      \AXC{$P(b) \seq P(b) $} \RightLabel{$\ex_r$}
      \UIC{$P(b) \seq \ex x. P(x) $} \RightLabel{$\vee_l$}
  \BIC{$(P(a) \vee P(b)) \seq \ex x. P(x) $} \RightLabel{$\imp_r$}
  \UIC{$\seq (P(a) \vee P(b)) \imp \ex x. P(x) $}
\end{prooftree}
 
Using arrays to extract a Herbrand sequent, we get:
\begin{prooftree}
\AXC{$P(a) \seq P(a) $} \RightLabel{$\ex_r$}
      \AXC{$P(b) \seq P(b) $} \RightLabel{$\ex_r$}
  \BIC{$(P(a) \vee P(b)) \seq \langle P(a),P(b) \rangle $} \RightLabel{$\imp_r$}
  \UIC{$\seq (P(a) \vee P(b)) \imp \langle P(a),P(b) \rangle $}
\end{prooftree}

The extracted \emph{Herbrand array sequent} is the end-sequent of the proof above. 

Classically, to obtain a Herbrand sequent (without arrays), we expand the arrays, distributing their contexts over their elements:
$$
 \seq (P(a) \vee P(b)) \imp P(a), (P(a) \vee P(b)) \imp P(b)  
$$

Unfortunately, this Herbrand sequent is not intuitionistically valid. In fact, it is not even an intuitionistic sequent.
We could replace the comma by a disjunction:
$$
 \seq ((P(a) \vee P(b)) \imp P(a)) \vee ((P(a) \vee P(b)) \imp P(b))  
$$
but although this is now an intuitionistic sequent, it is still not valid in intuitionistic logic.

What we really need is simply to refrain from expanding arrays. We construct an \emph{intuitionistic Herbrand sequent} by locally replacing arrays by disjunctions or conjunctions in the Herbrand array sequent, thus obtaining an intuitionistically valid propositional sequent:
$$
\seq (P(a) \vee P(b)) \imp (P(a) \vee P(b)) 
$$

\begin{theorem}
 If $s$ is an intuitionistically valid sequent, then there is a (valid) intuitionistic Herbrand sequent of $s$.
\end{theorem}
\begin{proof}
 Easy, by construction, extracting the intuitionistic Herbrand sequent from the proof of $s$, as exemplified above.
\end{proof}

The converse of this theorem should be a bit harder to prove, although not impossible.


\section{Speed-Ups}

All assymptotic speed-ups of {\CERes} should hold for {\iCERes} as well, as long as the example proof sequences used to prove the speed-ups are intuitionistic or, if not, as long as we can find intuitionistic versions of these sequences... 


\section{Conclusions}

{\iCERes} is a straightforward and minimal modification of {\CERes} that works for intuitionistic logic. Since the output proofs contain only propositional cuts, an intuitionistic Herbrand sequent can be directly extracted from this proof, with no need to eliminate the remaining cuts.


\vspace{-10pt}
\bibliographystyle{plain}
\bibliography{Bibliography}

\end{document}
